VERS5 
NIL 
((LISTINDUCTION LISPAX#29) (LISTINDUCTIONDEF LISPAX#33) (SEXPINDUCTION LISPAX#34) (SEXPINDUCTIONDEF LISPAX#35) (LISTDEF LISPAX#40) (APPENDEF LISPAX#42) (LISTAPPEND LISPAX#43) (ALLPDEF LISPAX#47) (SOMEPDEF LISPAX#48) (MAPCARDEF LISPAX#49) (MKALIST LISPAX#53) (ASSOCDEF LISPAX#55) (MEMBERDEF LISPAX#58) (SIMPINFO LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#38 LISPAX#39 LISPAX#40 LISPAX#42 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#51 LISPAX#56)) (NIL . (DECL CAR (UNARYNAME: CAR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CAR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CAR)) . LISPAX#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 1 .)(NIL . (DECL CDR (UNARYNAME: CDR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CDR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CDR)) . LISPAX#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 2 .)(NIL . (DECL ATOM (UNARYNAME: ATOM) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ATOM . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ATOM)) . LISPAX#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 3 .)(NIL . (DECL NULL (UNARYNAME: NULL) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((NULL . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . NULL)) . LISPAX#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 4 .)(NIL . (DECL LISTP (UNARYNAME: LISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((LISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . LISTP)) . LISPAX#5 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 5 .)(NIL . (DECL ALISTP (UNARYNAME: ALISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ALISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ALISTP)) . LISPAX#6 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 6 .)(NIL . (DECL SEXP (UNARYNAME: SEXP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((SEXP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . SEXP)) . LISPAX#7 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 7 .)(NIL . (DECL (U V W) (TYPE: (TY& . GROUND)) (SORT: (TM& . LISTP))) . ((W . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (V . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (U . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) LISTP) . NIL . NIL . NIL . LISPAX . NIL . 8 .)(NIL . (DECL (X Y Z) (TYPE: (TY& . GROUND)) (SORT: (TM& . SEXP))) . ((Z . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (Y . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (X . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) SEXP) . NIL . NIL . NIL . LISPAX . NIL . 9 .)(NIL . (DECL (XA YA ZA) (TYPE: (TY& . GROUND)) (SORT: (TM& . ATOM))) . ((ZA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (YA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (XA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) ATOM) . NIL . NIL . NIL . LISPAX . NIL . 10 .)(NIL . (DECL (A B C) (TYPE: (TY& . GROUND))) . ((C . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#11 . NIL . VARIABLE .)) (B . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#11 . NIL . VARIABLE .)) (A . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#11 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 11 .)(NIL . (DECL (PHI) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((PHI . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#12 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 12 .)(NIL . (DECL CONS (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: |.|) (PREFIXNAME: CONS) (BINDINGPOWER: 850)) . ((CONS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 850) (PREFIX& . CONS) (INFIX& . |.|)) . LISPAX#13 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 13 .)(|∀XA.SEXP XA| . (AXIOM (TM& . |∀XA.SEXP XA|)) . (ATOM SEXP ZA YA XA) . NIL . (LISPAX#14) . NIL . LISPAX . NIL . 14 .)(|∀U.SEXP U| . (AXIOM (TM& . |∀U.SEXP U|)) . (LISTP SEXP W V U) . NIL . (LISPAX#15) . NIL . LISPAX . NIL . 15 .)(|∀X U.LISTP X.U| . (AXIOM (TM& . |∀X U.LISTP X.U|)) . (LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#16) . NIL . LISPAX . NIL . 16 .)(|∀U.¬NULL U⊃LISTP CDR U| . (AXIOM (TM& . |∀U.¬NULL U⊃LISTP CDR U|)) . (CDR NULL LISTP W V U) . NIL . (LISPAX#17) . NIL . LISPAX . NIL . 17 .)(|∀U.¬NULL U⊃SEXP CAR U| . (AXIOM (TM& . |∀U.¬NULL U⊃SEXP CAR U|)) . (CAR NULL LISTP SEXP W V U) . NIL . (LISPAX#18) . NIL . LISPAX . NIL . 18 .)(|∀X.¬ATOM X⊃SEXP CAR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CAR X|)) . (CAR ATOM SEXP Z Y X) . NIL . (LISPAX#19) . NIL . LISPAX . NIL . 19 .)(|∀X.¬ATOM X⊃SEXP CDR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CDR X|)) . (CDR ATOM SEXP Z Y X) . NIL . (LISPAX#20) . NIL . LISPAX . NIL . 20 .)(|∀X Y.SEXP X.Y| . (AXIOM (TM& . |∀X Y.SEXP X.Y|)) . (SEXP Z Y X CONS) . NIL . (LISPAX#21) . NIL . LISPAX . NIL . 21 .)(|∀X Y.¬ATOM X.Y| . (AXIOM (TM& . |∀X Y.¬ATOM X.Y|)) . (ATOM SEXP Z Y X CONS) . NIL . (LISPAX#22) . NIL . LISPAX . NIL . 22 .)(|∀X U.¬NULL X.U| . (AXIOM (TM& . |∀X U.¬NULL X.U|)) . (NULL LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#23) . NIL . LISPAX . NIL . 23 .)(|∀U.NULL U⊃U=NIL| . (AXIOM (TM& . |∀U.NULL U⊃U=NIL|)) . (NULL LISTP W V U) . NIL . (LISPAX#24) . NIL . LISPAX . NIL . 24 .)(|∀X Y.CAR (X.Y)=X| . (AXIOM (TM& . |∀X Y.CAR (X.Y)=X|)) . (CAR SEXP Z Y X CONS) . NIL . (LISPAX#25) . NIL . LISPAX . NIL . 25 .)(|∀X Y.CDR (X.Y)=Y| . (AXIOM (TM& . |∀X Y.CDR (X.Y)=Y|)) . (CDR SEXP Z Y X CONS) . NIL . (LISPAX#26) . NIL . LISPAX . NIL . 26 .)(|∀U.¬NULL U⊃CAR U.CDR U=U| . (AXIOM (TM& . |∀U.¬NULL U⊃CAR U.CDR U=U|)) . (CAR CDR NULL LISTP W V U CONS) . NIL . (LISPAX#27) . NIL . LISPAX . NIL . 27 .)(|∀X.¬ATOM X⊃CAR X.CDR X=X| . (AXIOM (TM& . |∀X.¬ATOM X⊃CAR X.CDR X=X|)) . (CAR CDR ATOM SEXP Z Y X CONS) . NIL . (LISPAX#28) . NIL . LISPAX . NIL . 28 .)(|∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))| . (AXIOM (TM& . |∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))|)) . (LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#29) . NIL . LISPAX . NIL . 29 .)(NIL . (DECL PARS (TYPE: (TY& . GROUND*))) . ((PARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#30 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 30 .)(NIL . (DECL (DF DF1 DF2) (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((DF2 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#31 . NIL . VARIABLE .)) (DF1 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#31 . NIL . VARIABLE .)) (DF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#31 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 31 .)(NIL . (DECL NILCASE (TYPE: (TY& . |(GROUND*)→(GROUND*)|))) . ((NILCASE . (|(GROUND*)→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 32 .)(|∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)=DEF(X,U,FUN(U,DF(X,PARS)),PARS)))| . (AXIOM (TM& . |∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)=DEF(X,U,FUN(U,DF(X,PARS)),PARS)))|)) . (LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#33 . NIL . VARIABLE .)) (DEF . (|(GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#33 . NIL . VARIABLE .))) . NIL . (LISPAX#33) . NIL . LISPAX . NIL . 33 .)(|∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))| . (AXIOM (TM& . |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))|)) . (ATOM SEXP Z Y X PHI CONS) . NIL . (LISPAX#34) . NIL . LISPAX . NIL . 34 .)(|∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y.(ATOM X⊃ FUN(X,PARS)=ATOMCASE(X,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,PARS)), FUN(Y,DF2(X,PARS)),PARS)))| . (AXIOM (TM& . |∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y.(ATOM X⊃ FUN(X,PARS)=ATOMCASE(X,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,PARS)), FUN(Y,DF2(X,PARS)),PARS)))|)) . (ATOM LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE FUN DEF (DEFSEXP . (|(GROUND⊗GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#35 . NIL . VARIABLE .)) (ATOMCASE . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#35 . NIL . VARIABLE .))) . NIL . (LISPAX#35) . NIL . LISPAX . NIL . 35 .)(NIL . (DECL LIST (TYPE: (TY& . |(GROUND*)→GROUND|)) (SYNTYPE: CONSTANT)) . ((LIST . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#36 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 36 .)(NIL . (DECL LST (TYPE: (TY& . GROUND*))) . ((LST . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 37 .)(|LIST(())=NIL| . (AXIOM (TM& . |LIST(())=NIL|)) . (LIST) . NIL . (LISPAX#38) . NIL . LISPAX . NIL . 38 .)(|∀LST.LISTP LIST(LST)| . (AXIOM (TM& . |∀LST.LISTP LIST(LST)|)) . (LISTP LIST LST) . NIL . (LISPAX#39) . NIL . LISPAX . NIL . 39 .)(|∀X LST.LIST(X,LST)=X.LIST(LST)| . (AXIOM (TM& . |∀X LST.LIST(X,LST)=X.LIST(LST)|)) . (SEXP Z Y X CONS LIST LST) . NIL . (LISPAX#40) . NIL . LISPAX . NIL . 40 .)(NIL . (DECL APPEND (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (INFIXNAME: *) (BINDINGPOWER: 840)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . LISPAX#41 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 41 .)(|∀X U V.NIL*V=V∧X.U*V=X.(U*V)| . (DEFAX APPEND (TM& . |∀X U V.NIL*V=V∧X.U*V=X.(U*V)|)) . (LISTP SEXP W V U Z Y X CONS (APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . *)) . LISPAX#42 . NIL . DEFINED .))) . NIL . (LISPAX#42) . NIL . LISPAX . NIL . 42 .)(|∀U V.LISTP U*V| . (AXIOM (TM& . |∀U V.LISTP U*V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#43) . NIL . LISPAX . NIL . 43 .)(|∀U.U*NIL=U| . (AXIOM (TM& . |∀U.U*NIL=U|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#44) . NIL . LISPAX . NIL . 44 .)(|∀X V.X.NIL*V=X.V| . (AXIOM (TM& . |∀X V.X.NIL*V=X.V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#45) . NIL . LISPAX . NIL . 45 .)(NIL . (DECL (ALLP SOMEP) (SYNTYPE: CONSTANT) (TYPE: (TY& . |((@PHI)⊗GROUND)→TRUTHVAL|))) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#46 . NIL . CONSTANT .)) (ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#46 . NIL . CONSTANT .)) PHI) . NIL . NIL . NIL . LISPAX . NIL . 46 .)(|∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)| . (DEFAX ALLP (TM& . |∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)|)) . (LISTP SEXP W V U Z Y X PHI CONS (SOMEP . LISPAX#46) (ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#47 . NIL . DEFINED .))) . NIL . (LISPAX#47) . NIL . LISPAX . NIL . 47 .)(|∀PHI X U.¬SOMEP(PHI,NIL)∧SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))| . (DEFAX SOMEP (TM& . |∀PHI X U.¬SOMEP(PHI,NIL)∧SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))|)) . (LISTP SEXP W V U Z Y X PHI CONS (SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#48 . NIL . DEFINED .))) . NIL . (LISPAX#48) . NIL . LISPAX . NIL . 48 .)(|∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)| . (DEFAX MAPCAR (TM& . |∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)|)) . (LISTP SEXP W V U Z Y X CONS (MAPCAR . (|((GROUND→GROUND)⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#49 . NIL . DEFINED .)) (FN . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#49 . NIL . VARIABLE .))) . NIL . (LISPAX#49) . NIL . LISPAX . NIL . 49 .)(NIL . (DECL (ALIST A0 A1 A2) (TYPE: (TY& . GROUND)) (SORT: (TM& . ALISTP))) . ((A2 . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . LISPAX#50 . NIL . VARIABLE .)) (A1 . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . LISPAX#50 . NIL . VARIABLE .)) (A0 . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . LISPAX#50 . NIL . VARIABLE .)) (ALIST . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . LISPAX#50 . NIL . VARIABLE .)) ALISTP) . NIL . NIL . NIL . LISPAX . NIL . 50 .)(|∀ALIST.LISTP ALIST| . (AXIOM (TM& . |∀ALIST.LISTP ALIST|)) . (LISTP ALISTP A2 A1 A0 ALIST) . NIL . (LISPAX#51) . NIL . LISPAX . NIL . 51 .)(|∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)| . (AXIOM (TM& . |∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)|)) . (CAR ATOM NULL ALISTP A2 A1 A0 ALIST) . NIL . (LISPAX#52) . NIL . LISPAX . NIL . 52 .)(|∀XA Y ALIST.ALISTP (XA.Y).ALIST| . (AXIOM (TM& . |∀XA Y ALIST.ALISTP (XA.Y).ALIST|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS A2 A1 A0 ALIST) . NIL . (LISPAX#53) . NIL . LISPAX . NIL . 53 .)(NIL . (DECL ASSOC (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#54 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 54 .)(|∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))| . (DEFAX ASSOC (TM& . |∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS A2 A1 A0 ALIST (ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#55 . NIL . DEFINED .))) . NIL . (LISPAX#55) . NIL . LISPAX . NIL . 55 .)(|∀X ALIST.SEXP ASSOC(X,ALIST)| . (AXIOM (TM& . |∀X ALIST.SEXP ASSOC(X,ALIST)|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS A2 A1 A0 ALIST ASSOC) . NIL . (LISPAX#56) . NIL . LISPAX . NIL . 56 .)(NIL . (DECL MEMBER (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#57 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 57 .)(|∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))| . (DEFAX MEMBER (TM& . |∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))|)) . (LISTP SEXP W V U Z Y X CONS (MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#58 . NIL . DEFINED .))) . NIL . (LISPAX#58) . NIL . LISPAX . NIL . 58 .)